A, B:Realizer. R-frame-compat(A;B)  Prop 

latex

Definitions

x:A. B(x), t  T, Prop, R-frame-compat(A;B), if b t else f fi, P  Q, true, false, x. t(x), , Unit, P  Q, P & Q, x(s),

Lemmas

Reffect? wf, bool wf, eqtt to assert, Rframe? wf, Id wf, Rframe-x wf, Reffect-x wf, l member wf, Knd wf, Reffect-knd wf, Rframe-L wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, Raframe? wf, Raframe-k wf, Raframe-L wf, Rrframe? wf, fpf-dom wf, id-deq wf, Reffect-ds wf, fpf-trivial-subtype-top, fpf wf, top wf, Rrframe-x wf, Rrframe-L wf, true wf, Rsends? wf, Rsframe? wf, IdLnk wf, Rsframe-lnk wf, Rsends-l wf, Rsframe-tag wf, map wf, decl-state wf, Rsends-ds wf, Rsends-T wf, decl-type wf, Rsends-dt wf, pi1 wf, Rsends-g wf, Rsends-knd wf, Rsframe-L wf, Rbframe? wf, Rbframe-k wf, Rbframe-L wf, Rpre? wf, Rpre-ds wf, locl wf, Rpre-a wf, es realizer wf